Curry-Howard 對應
program=證明 (proofs-as-programs)
型=命題 (formulae-as-types)
BHK 解釋 (Brouwer-Heyting-Kolmogorov 解釋) @ 直觀主義論理 computation - logic - space
table:對應
cut 規則 classifying morphism の合成。display map の引き戾し 置換 (substitution) 含意の導入規則 hom-tensor adjunction の餘單位 λ 抽象 含意の除去規則 hom-tensor adjunction の單位 (圈) 適用 cut 除去 hom-tensor adjunction の zigzag 恆等式 β 簡約
identity 除去 hom-tensor adjunction の zigzag 恆等式 η 變換
眞理値 subsingleton subterminal 對象。(-1)-truncated 對象 h-proposition。mere proposition
全稱量化 indexed 直積 依存積 依存積型
存在量化 indexed 非交和 依存和 依存和型
等値 bijection set object of isomorphisms 等値型
support set support object。(-1)-truncation propositional truncation。bracket type
n-image of morphism into terminal object。n-truncation n-truncation modality
propositional equality 對角寫像。對角部分集合。對角關係 道空閒對象 (Path) identity 型。道型 completely presented set 集合 離散對象。0-truncated 對象 h-level 2-type。集合。h-set 集合 equivalence relation を備へた集合 internal 0-亞群 Bishop set。setoid with its pseudo-equivalence relation an actual equivalence relation equivalence class。商集合 商 商型
高階 induction higher colimit 高階歸納型
0-truncated higher colimit quotient inductive type
preset identity 型を備へない型
眞理値の集合 部分對象分類子 type of propositions domain of discourse 宇宙 object classifier 型の宇宙
synthetic mathematics 領域特化埋め込み programming 言語
(-2)-truncated 對象
h-level 0-型
subterminal 對象
table:對應
論理式 命題 對象
證明 射
依存積 全稱量化
依存和 存在量化